YES 1.29
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule List
| ((isPrefixOf :: Eq a => [a] -> [a] -> Bool) :: Eq a => [a] -> [a] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] _ | = | True |
isPrefixOf | _ [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((isPrefixOf :: Eq a => [a] -> [a] -> Bool) :: Eq a => [a] -> [a] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (isPrefixOf :: Eq a => [a] -> [a] -> Bool) |
module List where
| import qualified Maybe import qualified Prelude
|
| isPrefixOf :: Eq a => [a] -> [a] -> Bool
isPrefixOf | [] vw | = | True |
isPrefixOf | vx [] | = | False |
isPrefixOf | (x : xs) (y : ys) | = | x == y && isPrefixOf xs ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy1100), Succ(xy400000)) → new_primPlusNat(xy1100, xy400000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy1100), Succ(xy400000)) → new_primPlusNat(xy1100, xy400000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy30000), Succ(xy40000)) → new_primMulNat(xy30000, Succ(xy40000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy30000), Succ(xy40000)) → new_primMulNat(xy30000, Succ(xy40000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy3000), Succ(xy4000)) → new_primEqNat(xy3000, xy4000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy3000), Succ(xy4000)) → new_primEqNat(xy3000, xy4000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs1(Left(xy300), Left(xy400), app(app(ty_@2, hc), hd), gd) → new_esEs3(xy300, xy400, hc, hd)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(app(ty_Either, db), dc)) → new_esEs1(xy302, xy402, db, dc)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(app(ty_@2, de), df)) → new_esEs3(xy302, xy402, de, df)
new_esEs2(Just(xy300), Just(xy400), app(ty_[], bag)) → new_esEs(xy300, xy400, bag)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(ty_Maybe, bcg)) → new_esEs2(xy301, xy401, bcg)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_Either, bdg), bdh), bdc) → new_esEs1(xy300, xy400, bdg, bdh)
new_esEs1(Left(xy300), Left(xy400), app(app(app(ty_@3, ge), gf), gg), gd) → new_esEs0(xy300, xy400, ge, gf, gg)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(ty_Maybe, fh), cd, dh) → new_esEs2(xy300, xy400, fh)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(app(ty_Either, ff), fg), cd, dh) → new_esEs1(xy300, xy400, ff, fg)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(ty_Maybe, dd)) → new_esEs2(xy302, xy402, dd)
new_esEs1(Right(xy300), Right(xy400), he, app(app(app(ty_@3, hg), hh), baa)) → new_esEs0(xy300, xy400, hg, hh, baa)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(ty_[], bdb), bdc) → new_esEs(xy300, xy400, bdb)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(app(app(ty_@3, bdd), bde), bdf), bdc) → new_esEs0(xy300, xy400, bdd, bde, bdf)
new_esEs1(Left(xy300), Left(xy400), app(app(ty_Either, gh), ha), gd) → new_esEs1(xy300, xy400, gh, ha)
new_esEs2(Just(xy300), Just(xy400), app(ty_Maybe, bbe)) → new_esEs2(xy300, xy400, bbe)
new_esEs1(Right(xy300), Right(xy400), he, app(app(ty_Either, bab), bac)) → new_esEs1(xy300, xy400, bab, bac)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(xy301, xy401, ea, eb, ec)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(ty_[], ce)) → new_esEs(xy302, xy402, ce)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(app(ty_Either, ed), ee), dh) → new_esEs1(xy301, xy401, ed, ee)
new_esEs(:(xy300, xy301), :(xy400, xy401), app(ty_Maybe, bh)) → new_esEs2(xy300, xy400, bh)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(app(ty_@2, eg), eh), dh) → new_esEs3(xy301, xy401, eg, eh)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(ty_[], bca)) → new_esEs(xy301, xy401, bca)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(app(ty_@2, bch), bda)) → new_esEs3(xy301, xy401, bch, bda)
new_esEs2(Just(xy300), Just(xy400), app(app(app(ty_@3, bah), bba), bbb)) → new_esEs0(xy300, xy400, bah, bba, bbb)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(app(ty_@2, ga), gb), cd, dh) → new_esEs3(xy300, xy400, ga, gb)
new_esEs2(Just(xy300), Just(xy400), app(app(ty_Either, bbc), bbd)) → new_esEs1(xy300, xy400, bbc, bbd)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(ty_[], fa), cd, dh) → new_esEs(xy300, xy400, fa)
new_esEs(:(xy300, xy301), :(xy400, xy401), ba) → new_esEs(xy301, xy401, ba)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(ty_Maybe, bea), bdc) → new_esEs2(xy300, xy400, bea)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(app(ty_Either, bce), bcf)) → new_esEs1(xy301, xy401, bce, bcf)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xy302, xy402, cf, cg, da)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(ty_[], dg), dh) → new_esEs(xy301, xy401, dg)
new_esEs1(Left(xy300), Left(xy400), app(ty_Maybe, hb), gd) → new_esEs2(xy300, xy400, hb)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_@2, beb), bec), bdc) → new_esEs3(xy300, xy400, beb, bec)
new_esEs(:(xy300, xy301), :(xy400, xy401), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(xy300, xy400, bc, bd, be)
new_esEs(:(xy300, xy301), :(xy400, xy401), app(app(ty_@2, ca), cb)) → new_esEs3(xy300, xy400, ca, cb)
new_esEs2(Just(xy300), Just(xy400), app(app(ty_@2, bbf), bbg)) → new_esEs3(xy300, xy400, bbf, bbg)
new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs0(xy301, xy401, bcb, bcc, bcd)
new_esEs(:(xy300, xy301), :(xy400, xy401), app(app(ty_Either, bf), bg)) → new_esEs1(xy300, xy400, bf, bg)
new_esEs1(Right(xy300), Right(xy400), he, app(ty_[], hf)) → new_esEs(xy300, xy400, hf)
new_esEs1(Left(xy300), Left(xy400), app(ty_[], gc), gd) → new_esEs(xy300, xy400, gc)
new_esEs1(Right(xy300), Right(xy400), he, app(app(ty_@2, bae), baf)) → new_esEs3(xy300, xy400, bae, baf)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(ty_Maybe, ef), dh) → new_esEs2(xy301, xy401, ef)
new_esEs1(Right(xy300), Right(xy400), he, app(ty_Maybe, bad)) → new_esEs2(xy300, xy400, bad)
new_esEs(:(xy300, xy301), :(xy400, xy401), app(ty_[], bb)) → new_esEs(xy300, xy400, bb)
new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(xy300, xy400, fb, fc, fd)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs(:(xy300, xy301), :(xy400, xy401), app(app(ty_Either, bf), bg)) → new_esEs1(xy300, xy400, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(xy300, xy301), :(xy400, xy401), app(app(app(ty_@3, bc), bd), be)) → new_esEs0(xy300, xy400, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(xy300, xy301), :(xy400, xy401), app(ty_Maybe, bh)) → new_esEs2(xy300, xy400, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy300, xy301), :(xy400, xy401), app(app(ty_@2, ca), cb)) → new_esEs3(xy300, xy400, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xy300), Just(xy400), app(app(ty_Either, bbc), bbd)) → new_esEs1(xy300, xy400, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xy300), Just(xy400), app(app(app(ty_@3, bah), bba), bbb)) → new_esEs0(xy300, xy400, bah, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(xy300), Just(xy400), app(ty_Maybe, bbe)) → new_esEs2(xy300, xy400, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(xy300), Just(xy400), app(app(ty_@2, bbf), bbg)) → new_esEs3(xy300, xy400, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xy300), Just(xy400), app(ty_[], bag)) → new_esEs(xy300, xy400, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_Either, bdg), bdh), bdc) → new_esEs1(xy300, xy400, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(app(ty_Either, bce), bcf)) → new_esEs1(xy301, xy401, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(app(app(ty_@3, bdd), bde), bdf), bdc) → new_esEs0(xy300, xy400, bdd, bde, bdf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs0(xy301, xy401, bcb, bcc, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(ty_Maybe, bcg)) → new_esEs2(xy301, xy401, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(ty_Maybe, bea), bdc) → new_esEs2(xy300, xy400, bea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(app(ty_@2, bch), bda)) → new_esEs3(xy301, xy401, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(app(ty_@2, beb), bec), bdc) → new_esEs3(xy300, xy400, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), app(ty_[], bdb), bdc) → new_esEs(xy300, xy400, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xy300, xy301), @2(xy400, xy401), bbh, app(ty_[], bca)) → new_esEs(xy301, xy401, bca)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(xy300), Left(xy400), app(app(ty_Either, gh), ha), gd) → new_esEs1(xy300, xy400, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xy300), Right(xy400), he, app(app(ty_Either, bab), bac)) → new_esEs1(xy300, xy400, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(app(ty_Either, db), dc)) → new_esEs1(xy302, xy402, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(app(ty_Either, ff), fg), cd, dh) → new_esEs1(xy300, xy400, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(app(ty_Either, ed), ee), dh) → new_esEs1(xy301, xy401, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Left(xy300), Left(xy400), app(app(app(ty_@3, ge), gf), gg), gd) → new_esEs0(xy300, xy400, ge, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Right(xy300), Right(xy400), he, app(app(app(ty_@3, hg), hh), baa)) → new_esEs0(xy300, xy400, hg, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(app(app(ty_@3, ea), eb), ec), dh) → new_esEs0(xy301, xy401, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(app(app(ty_@3, cf), cg), da)) → new_esEs0(xy302, xy402, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(app(app(ty_@3, fb), fc), fd), cd, dh) → new_esEs0(xy300, xy400, fb, fc, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(Left(xy300), Left(xy400), app(ty_Maybe, hb), gd) → new_esEs2(xy300, xy400, hb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(Right(xy300), Right(xy400), he, app(ty_Maybe, bad)) → new_esEs2(xy300, xy400, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(xy300), Left(xy400), app(app(ty_@2, hc), hd), gd) → new_esEs3(xy300, xy400, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(Right(xy300), Right(xy400), he, app(app(ty_@2, bae), baf)) → new_esEs3(xy300, xy400, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(Right(xy300), Right(xy400), he, app(ty_[], hf)) → new_esEs(xy300, xy400, hf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(Left(xy300), Left(xy400), app(ty_[], gc), gd) → new_esEs(xy300, xy400, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy300, xy301), :(xy400, xy401), ba) → new_esEs(xy301, xy401, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(xy300, xy301), :(xy400, xy401), app(ty_[], bb)) → new_esEs(xy300, xy400, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(ty_Maybe, dd)) → new_esEs2(xy302, xy402, dd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(ty_Maybe, fh), cd, dh) → new_esEs2(xy300, xy400, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(ty_Maybe, ef), dh) → new_esEs2(xy301, xy401, ef)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(app(ty_@2, de), df)) → new_esEs3(xy302, xy402, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(app(ty_@2, eg), eh), dh) → new_esEs3(xy301, xy401, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(app(ty_@2, ga), gb), cd, dh) → new_esEs3(xy300, xy400, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, cd, app(ty_[], ce)) → new_esEs(xy302, xy402, ce)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), app(ty_[], fa), cd, dh) → new_esEs(xy300, xy400, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@3(xy300, xy301, xy302), @3(xy400, xy401, xy402), cc, app(ty_[], dg), dh) → new_esEs(xy301, xy401, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba) → new_isPrefixOf(xy31, xy41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_isPrefixOf(:(xy30, xy31), :(xy40, xy41), ba) → new_isPrefixOf(xy31, xy41, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3